\begin{tabbing}
preinit1R\=\{\$x:ut2, \$a:ut2\}\+
\\[0ex]($i$; $X$; $T$; $x_{0}$; $P$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=@$i$ \=precondition for "\$a"(v:$T$):\+\+
\\[0ex]$\lambda$$s$,$v$. $P$($s$."\$x",$v$) State("\$x" : $X$) v
\-\\[0ex].@$i$ "\$x" initially $x_{0}$:$X$.nil)
\-
\end{tabbing}